Nuprl Lemma : w-state-after 11,40
w:World.
FairFifo
 (e:E. state_after(e) = (x,q. s(loc(e);time(e)+1).x(q - 1))  x:Idvartype(loc(e);x)) 
latex

Definitionst  T, x:A. B(x), time(e), #$n, , {x:A| B(x)} , x:AB(x), n+m, A  B, a < b, Void, P  Q, False, A, , Id, , r - s, loc(e), s(i;t).x, f(a), x.A(x), vartype(i;x), x. t(x), t.2, s = t, , state_after(e), E, FairFifo, World
Lemmasw-when-after, world wf, fair-fifo wf, w-E wf, pi2 wf, w-vartype wf, w-s wf, w-loc wf, qsub wf, int inc rationals, rationals wf, Id wf, le wf, nat wf, w-time wf

origin